Nuprl Lemma : neg_assoced 2,24
a:. (-a) ~ a 
latex

Definitionsa ~ b, x:A. B(x), P & Q, t  T, P  Q, P  Q, P  Q
Lemmasdivides invar 2, divides reflexivity, divides invar 1

origin